\begin{tabbing}
w{-}pred($w$;$e$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=if\= (time($e$) =$_{0}$ 0)\+\+
\\[0ex]then inr $\cdot$ 
\-\\[0ex]if\= isnull(a(loc($e$);time($e$) {-} 1))\+
\\[0ex]then w{-}pred($w$;$<$loc($e$), time($e$) {-} 1$>$)
\-\\[0ex]else inl $<$loc($e$), time($e$) {-} 1$>$ 
\\[0ex]fi 
\\[0ex]
\-\\[0ex]{\em clarification:}
\\[0ex]
\\[0ex]w{-}pred($w$;$e$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=if\= (w{-}time($w$; $e$) =$_{0}$ 0)\+\+
\\[0ex]then inr $\cdot$ 
\-\\[0ex]if\= w{-}isnull($w$; w{-}a($w$; w{-}loc($w$; $e$); (w{-}time($w$; $e$) {-} 1)))\+
\\[0ex]then w{-}pred($w$;$<$w{-}loc($w$; $e$), w{-}time($w$; $e$) {-} 1$>$)
\-\\[0ex]else inl $<$w{-}loc($w$; $e$), w{-}time($w$; $e$) {-} 1$>$ 
\\[0ex]fi 
\-\\[0ex]\emph{(recursive)}
\end{tabbing}